Here is a tentative to use path to define partition (that I renamed division because partition is a bit overloaded): https://github.com/affeldt-aist/analysis/blob/total_variation/theories/realfun.v#L680

I haven't yet completely ported the continuity proofs though (and the rest is still dirty but that can give a good idea of the difference).

The last commit redefines partition (renamed itv_partition to avoid overloading) using path and reproves the basic theory. The reimplementation is transparent enough so that the last bit of the development (about TV and continuity) is left unchanged.

(I just made a few comments to mark a few lemmas that made their way into master recently.)

(If the itv_partition/bounded_partition/total_variation looks stable enough, we could maybe make a separated PR to merge it asap?)

Cleaning up the duplicate lemmas and notations sounds good. Other than the admits, is there anything else required? I can make an attempt on those today/tomorrow.

I filled in that last admitted. The statement of the admit was incorrect. That is

 {within `[a,b], continuous f} <-> {in `],a,b[, continuous f} /\ f ^'+a --> f a /\ f^'-b --> f b

is false. It needs a<b. Note that strictness is required, as even when a = b the LHS is trivially true, and the boundary conditions on the RHS are non-trivial. Thankfully a<b was already in scope, so it's simple to fix.

I've been working in Coq for 4 years now, and I'm still regularly caught of guard by how pedantic it is. Every time I try to use admits in my workflow I make a mistake like this. I'm just glad this one didn't involve any major rework.

I made a first pass for minor checks.
I could streamline a few proof scripts, fix comments
and naming, do some renaming, remove one or two unused lemmas.
The lemma path_lt_last_filter (my bad) still looks a bit ad hoc
but I couldn't find a generalization right away.
The name total_variation_jordan_decompE does not really
correspond to the elements used in the statement.
What about bounded_variation_neg_tvE?

Changed jordan_decompE lemma to be

Lemma bounded_variation_pos_neg_tvE a b f : BV a b f ->
  {in `[a, b], f =1 (fine \o pos_tv a f) \- (fine \o neg_tv a f)}.

which is a little bit more obvious. As far as path_lt_last_filter goes, I agree it doesn't yield an immediate generalization in this context. I'm not sure how to improve it, so I'm fine with it's current state.

@IshiguroYoshihro Since you have been playing around with the definitions in this PR, could you take a quick look to see if there is something we can improve?

cd4bf11
is just the observation that we can write variation with next and prev from path.v.
This feels natural and I was therefore hoping that it would help reduce the size of the proof of variation_itv_partitionLR
which is the only lemma that uses variationE (variation using zip) but I failed.
The proof is getting much longer because of low-level manipulations of index and nth (that shows up because
of next_nth and prev_nth). Am I using the path library the wrong way?
In any case, aren't variation_next and variation_prev worth keeping around?

Oh, nice. A bit sad it doesn't clean up the proof, but it should allow for nicer "term-by-term" comparisons in the future, so you should merge those in regardless.